Search for: All records

Scenario-inding tools like the Alloy Analyzer are widely used in numerous concrete domains like security, network analysis, UML analysis, and so on. They can help to verify properties and, more generally, aid in exploring a system’s behavior. While scenario inders are valuable for their ability to produce concrete examples, individual scenarios only give insight into what is possible, leaving the user to make their own conclusions about what might be necessary. This paper enriches scenario inding by allowing users to ask łwhy?ž and łwhy not?ž questions about the examples they are given. We show how to distinguish parts of an example that cannot be consistently removed (or changed) from those that merely relect underconstraint in the speciication. In the former case we show how to determine which elements of the speciication and which other components of the example together explain the presence of such facts. This paper formalizes the act of computing provenance in scenario- inding. We present Amalgam, an extension of the popular Alloy scenario-inder, which implements these foundations and provides interactive exploration of examples. We also evaluate Amalgam’s algorithmics on a variety of both textbook and real-world examples. 

Model-finders such as SAT-solvers are attractive for produc- ing concrete models, either as sample instances or as counterexamples when properties fail. However, the generated model is arbitrary. To ad- dress this, several research efforts have proposed principled forms of output from model-finders. These include minimal and maximal models, unsat cores, and proof-based provenance of facts. While these methods enjoy elegant mathematical foundations, they have not been subjected to rigorous evaluation on users to assess their utility. This paper presents user studies of these three forms of output performed on advanced students. We find that most of the output forms fail to be effective, and in some cases even actively mislead users. To make such studies feasible to run frequently and at scale, we also show how we can pose such studies on the crowdsourcing site Mechanical Turk. 

Perovskite light‐emitting diodes (PeLEDs) have received great attention for their potential as next‐generation display technology. While remarkable progress has been achieved in green, red, and near‐infrared PeLEDs with external quantum efficiencies (EQEs) exceeding 20%, obtaining high performance blue PeLEDs remains a challenge. Poor charge balance due to large charge injection barriers in blue PeLEDs has been identified as one of the major roadblocks to achieve high efficiency. Here band edge control of perovskite emitting layers for blue PeLEDs with enhanced charge balance and device performance is reported. By using organic spacer cations with different dipole moments, that is, phenethyl ammonium (PEA), methoxy phenethyl ammonium (MePEA), and 4‐fluoro phenethyl ammonium (4FPEA), the band edges of quasi‐2D perovskites are tuned without affecting their band gaps. Detailed characterization and computational studies have confirmed the effect of dipole moment modification to be mostly electrostatic, resulting in changes in the ionization energies of ≈0.45 eV for MePEA and ≈ −0.65 eV for 4FPEA based thin films relative to PEA‐based thin films. With improved charge balance, blue PeLEDs based on MePEA quasi‐2D perovskites show twofold increase of the EQE as compared to the control PEA based devices.